Lurch Deductive Engine

Tutorial: Pattern matching

Pattern matching

This tutorial assumes you know how to construct LC instances; if not, see the tutorial on Constructing LCs. This tutorial covers how to use the Matching module to do pattern matching on LCs. If you are unfamiliar with the concept of pattern matching, follow that link to the Matching module and read that entire page of documentation first (although you can skip the final section, entitled "Technical details").

(Each piece of sample code below is written as if it were a script sitting in the root folder of this source code repository, and run from there with the command-line tools node. If you place your scripts in another folder, you will need to adjust the path in each import statement accordingly. If you have not yet set up a copy of this repository with the appropriate Node.js version installed, see our GitHub README, which explains how to do so.)

Constructing patterns and expressions

A matching problem is built from a set of pattern-expression pairs. We thus need to be able to construct both patterns and expressions. Expressions, of course, we already know how to construct; they are instance of the subclass of LogicConcept that is called Expression! More specifically, if you construct an LC using the fromPutdown() function and simply don't use any of the notation for Environments or Declarations, you are guaranteed to get only (an array of) Expressions as the result.


import { LogicConcept } from './src/index.js'

const [ expr1, expr2 ] = LogicConcept.fromPutdown( 'atomic   (not atomic)' )
console.log( expr1.toPutdown() )
console.log( expr2.toPutdown() )

// Console output:
atomic
(not atomic)

To construct a pattern, first build it as an expression, and then mark zero or more of its descendants as metavariables. For example, if you want the pattern $f(x)$, where both $f$ and $x$ are metavariables, you could proceed as follows.


import { Matching } from './src/index.js'

const pat = LogicConcept.fromPutdown( '(f x)' )[0]
pat.child( 0 ).makeIntoA( Matching.metavariable )
pat.child( 1 ).makeIntoA( Matching.metavariable )
console.log( pat.toPutdown() )

// Console output:
(f +{"_type_LDE MV":true}
 x +{"_type_LDE MV":true}
)

If you wanted every instance of a certain symbol in a large expression to be marked as a metavariable, you could use code like the following to be concise about it.


const f = LogicConcept.fromPutdown( 'f' )[0]
pat.descendantsSatisfying( d => d.equals( f ) )
   .map( d => d.makeIntoA( Matching.metavariable ) )

Building a matching problem

A matching problem is a set of constraints. Let's build a small matching problem from just one constraint, the pattern $f(x)$ from above matched with the expression expr2, which was (not atomic). Since they are both a unary function applied to one argument, and both $f$ and $x$ were marked as metavariables, the problem should have exactly one solution.


let P = new Matching.Problem( pat, expr2 )
console.log( P )

// Console output:
Problem {
  constraints: [ Constraint { _pattern: Application, _expression: Application } ]
}

Notice that the output above is not so helpful, because it just classifies the pattern and expression as instances of the Application class, which is accurate but not very specific. We can get a more helpful and more compact rendering of the Problem using its toString() member function, explicitly or implicitly.


console.log( P.toString() ) // explicit toString() call
console.log( `P = ${P}` )   // implicit toString() call

// Console output:
{
	3  ((f__ x__),(not atomic))
}
P = {
	3  ((f__ x__),(not atomic))
}

The notation is mostly straightforward; we have a set {...} of Constraints, containing just one member, the pattern-expression pair ($f(x)$,(not atomic)). But the notation for $f(x)$ is not (f x) as one might expect, but rather (f__ x__), for the following reason. As you can see from earlier output, metavariables are marked as such using an attribute that makes their putdown notation cumbersome. The toString() method for the Problem class replaces that cumbersome notation with a double underscore, to make it easy to identify metavariables on sight without taking up much space in the output.

We now have a matching problem that we can ask to solve itself.

Solving matching problems

Because solving matching problems can be a slow process, it would not be a good design if you were forced to compute all solutions at once. Thus the Problem class gives you the opportunity to compute solutions one at a time, and you can stop at any point, using the standard JavaScript feature of a "generator."

If you're unfamiliar with the idea of generators, you can fall back on the simpler method of computing all solutions at once and placing them in a standard JavaScript array. Simply apply the built-in JavaScript Array.from() function to convert the solution generator to an array of all of its results. Notice how solutions also have a more helpful output notation if you use their toString() function, either implicitly or explicitly. (Later we will see how to generate solutions one at a time.)


let sols = Array.from( P.solutions() )
console.log( `P -> [${sols}]` )

// Console output:
P -> [{(f__,not),(x__,atomic)}]

The above notation means that there is one solution, the substitution function expressed as the set of ordered pairs { (f__,not), (x__,atomic) }. (The suffix /cc{} means that there are no CaptureConstraints that apply to this solution.)

You can, of course, query the individual components of the Solution, with its API, as in the following example.


console.log( 'Number of solutions to P:', sols.length )
const sol1 = sols[0]
console.log( 'Metavariables in the solution:', sol1.domain() )
console.log( 'Instantiation for f:', sol1.get( 'f' ).toPutdown() )
console.log( 'Instantiation for x:', sol1.get( 'x' ).toPutdown() )

// Console output:
Number of solutions to P: 1
Metavariables in the solution: Set(2) { 'x', 'f' }
Instantiation for f: not
Instantiation for x: atomic

When there are no solutions

Of course, we can also form matching problems that have no solutions. For example, the form $f(x)$ would not match the atomic expression expr1 above.


sols = new Matching.Problem( pat, expr1 ).solutions()
console.log( 'Solutions:', Array.from( sols ) )

// Console output:
Solutions: []

A more complex example

The main functionality of the Matching module is covered above, but we do a more substantial example here in order to show the full functionality and complexity of the module.

We would like to match the pattern $P(x)$ to the expression $f(a,a)$, but we are now no longer considering $P(x)$ to mean "a metavariable $P$ applied to a metavariable $x$," but rather "an expression function $P$ applied to a metavariable $x$." (Recall the notion of expression functions defined in the documentation for the Matching module). We thus cannot simply parse the putdown notation (P x), flag P and x as metavariables, and move on, because that would have the wrong meaning. There is a special function in the Matching module for creating expressions like $P(x)$, which do not mean regular function application of $P$ to $x$, but application of $P$ as an expression function to the expression $x$. The function is called newEFA(), for "new expression function application."


// pattern
const mvP = LogicConcept.fromPutdown( 'P' )[0].asA( Matching.metavariable )
const mvx = LogicConcept.fromPutdown( 'x' )[0].asA( Matching.metavariable )
const Pofx = Matching.newEFA( mvP, mvx )

// expression
const faa = LogicConcept.fromPutdown( '(f a a)' )[0]

// problem
P = new Matching.Problem( Pofx, faa )
console.log( P.toString() )

// Console output:
{
	4  ((@ P__ x__),(f a a))
}

It's a fun puzzle to stop at this point and try to figure out what all the valid solutions to this matching problem are! Once you're ready for the spoiler, scroll down.

We will also use this opportunity to see how to generate solutions one at a time, rather than forcing the Matching module to compute all of them before we get to see any of them. We will use a loop, which computes one solution for each iteration of the loop, right before that iteration of the loop. If you need only one or two of the solutions, you could use break to terminate the loop early, and the remainder of the solutions would not be computed, thus not wasting any computation time.


let counter = 0
for ( let solution of P.solutions() ) {
    console.log( `Solution ${++counter}: ${solution}` )
    // For example, if you needed only two solutions, we could do:
    // if ( counter == 2 ) break
}

// Console output:
Solution 1: {(P__,(𝝺 v1 , (f a a)))}
Solution 2: {(P__,(𝝺 v1 , v1)),(x__,(f a a))}
Solution 3: {(P__,(𝝺 v4 , (v4 a a))),(x__,f)}
Solution 4: {(P__,(𝝺 v4 , (f v4 a))),(x__,a)}
Solution 5: {(P__,(𝝺 v4 , (f a v4))),(x__,a)}
Solution 6: {(P__,(𝝺 v4 , (f v4 v4))),(x__,a)}

To clarify the meaning of the notation used in the output above, we repeat the same 6 solutions here, in more natural mathematical notation:

  • $P$ could be the constant function that always returns $f(a,a)$
  • $P$ could be the identity function and $x$ would be $f(a,a)$
  • $P$ could be the function $v\mapsto v(a,a)$ and $x$ would be $f$
  • $P$ could be the function $v\mapsto f(v,a)$ and $x$ would be $a$
  • $P$ could be the function $v\mapsto f(a,v)$ and $x$ would be $a$
  • $P$ could be the function $v\mapsto f(v,v)$ and $x$ would be $a$